Nuprl Lemma : tree_subtype
4,23
postcript
pdf
E
:Type. Tree(
E
)
tree_con(
E
;Tree(
E
))
latex
Definitions
t
T
,
Tree(
E
)
,
S
T
,
x
:
A
.
B
(
x
)
,
tree_con(
E
;
T
)
Lemmas
tree
wf
origin
E:Type. Tree(E) 
tree_con(E;Tree(E)) E:Type. Tree(E) tree_con(E;Tree(E)) 
T Tx:A. B(x)